FDL - Nuprl Lemma : es-in-port-receives

Nuprl Lemma : es-in-port-receives

es:ES, l:IdLnk, tg:Id, A:Type.
(

e:E. (kind(e) = rcv(l,tg)

Knd)

(valtype(e)

r A))

(

e:E. (

(e

es-in-port(es;l;tg)))

(

isrcv(e)))

Definitions x:A. B(x), IdLnk, P Q, t T, , P Q, P & Q, {T}, A c B

Lemmas assert wf, es-E wf, Knd wf, es-kind wf, rcv wf, es-valtype wf, Id wf, event system wf, es-is-interface-in-port, es-kind-rcv, es-is-interface wf, es-in-port wf